Left Termination of the query pattern
hidden_flatten(g,a,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 185 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 267 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇒, 26 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 257 ms)
↳10 QDP
↳11 QDPOrderProof (⇔, 210 ms)
↳12 QDP
↳13 DependencyGraphProof (⇔, 0 ms)
↳14 TRUE

(0) Obligation:

Clauses:

hidden_flatten([], L, L).
hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F))).
hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L).

Query: hidden_flatten(g,a,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

pB([], X1, X1, X2, X3, X4) :- hidden_flattenA(.(X2, X3), X1, X4).
pB(.(.(X1, X2), X3), X4, X5, X6, X7, X8) :- hidden_flattenC(X3, X4, X9).
pB(.(.(X1, X2), X3), X4, X5, X6, X7, X8) :- ','(hidden_flattencC(X3, X4, X9), pB(.(X1, X2), X9, X5, X6, X7, X8)).
pB(.(X1, X2), X3, .(X1, X4), X5, X6, X7) :- hidden_flattenC(X2, X3, X4).
pB(.(X1, X2), X3, .(X1, X4), X5, X6, X7) :- ','(hidden_flattencC(X2, X3, X4), hidden_flattenA(.(X5, X6), .(X1, X4), X7)).
hidden_flattenC(.(.(X1, X2), X3), X4, X5) :- hidden_flattenC(X3, X4, X6).
hidden_flattenC(.(.(X1, X2), X3), X4, X5) :- ','(hidden_flattencC(X3, X4, X6), hidden_flattenA(.(X1, X2), X6, X5)).
hidden_flattenC(.(X1, X2), X3, .(X1, X4)) :- hidden_flattenC(X2, X3, X4).
hidden_flattenA(.(.(X1, X2), X3), X4, X5) :- pB(X3, X4, X6, X1, X2, X5).
hidden_flattenA(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) :- pB(X4, X5, X7, X2, X3, X6).
hidden_flattenA(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) :- hidden_flattenA(X3, X4, X5).

Clauses:

hidden_flattencA([], X1, X1).
hidden_flattencA(.(.(X1, X2), X3), X4, X5) :- qcB(X3, X4, X6, X1, X2, X5).
hidden_flattencA(.(X1, []), X2, .(X1, X2)).
hidden_flattencA(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) :- qcB(X4, X5, X7, X2, X3, X6).
hidden_flattencA(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) :- hidden_flattencA(X3, X4, X5).
qcB([], X1, X1, X2, X3, X4) :- hidden_flattencA(.(X2, X3), X1, X4).
qcB(.(.(X1, X2), X3), X4, X5, X6, X7, X8) :- ','(hidden_flattencC(X3, X4, X9), qcB(.(X1, X2), X9, X5, X6, X7, X8)).
qcB(.(X1, X2), X3, .(X1, X4), X5, X6, X7) :- ','(hidden_flattencC(X2, X3, X4), hidden_flattencA(.(X5, X6), .(X1, X4), X7)).
hidden_flattencC([], X1, X1).
hidden_flattencC(.(.(X1, X2), X3), X4, X5) :- ','(hidden_flattencC(X3, X4, X6), hidden_flattencA(.(X1, X2), X6, X5)).
hidden_flattencC(.(X1, X2), X3, .(X1, X4)) :- hidden_flattencC(X2, X3, X4).

Afs:

hidden_flattenA(x1, x2, x3)  =  hidden_flattenA(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
hidden_flattenA_in: (b,f,f)
pB_in: (b,f,f,b,b,f)
hidden_flattenC_in: (b,f,f)
hidden_flattencC_in: (b,f,f)
hidden_flattencA_in: (b,f,f)
qcB_in: (b,f,f,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3), X4, X5) → U12_GAA(X1, X2, X3, X4, X5, pB_in_gaagga(X3, X4, X6, X1, X2, X5))
HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3), X4, X5) → PB_IN_GAAGGA(X3, X4, X6, X1, X2, X5)
PB_IN_GAAGGA([], X1, X1, X2, X3, X4) → U1_GAAGGA(X1, X2, X3, X4, hidden_flattenA_in_gaa(.(X2, X3), X1, X4))
PB_IN_GAAGGA([], X1, X1, X2, X3, X4) → HIDDEN_FLATTENA_IN_GAA(.(X2, X3), X1, X4)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → U13_GAA(X1, X2, X3, X4, X5, X6, pB_in_gaagga(X4, X5, X7, X2, X3, X6))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → PB_IN_GAAGGA(X4, X5, X7, X2, X3, X6)
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U2_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattenC_in_gaa(X3, X4, X9))
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → HIDDEN_FLATTENC_IN_GAA(X3, X4, X9)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → U8_GAA(X1, X2, X3, X4, X5, hidden_flattenC_in_gaa(X3, X4, X6))
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → HIDDEN_FLATTENC_IN_GAA(X3, X4, X6)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_in_gaa(X3, X4, X6))
U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → U10_GAA(X1, X2, X3, X4, X5, hidden_flattenA_in_gaa(.(X1, X2), X6, X5))
U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → HIDDEN_FLATTENA_IN_GAA(.(X1, X2), X6, X5)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → U14_GAA(X1, X2, X3, X4, X5, hidden_flattenA_in_gaa(X3, X4, X5))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → HIDDEN_FLATTENA_IN_GAA(X3, X4, X5)
HIDDEN_FLATTENC_IN_GAA(.(X1, X2), X3, .(X1, X4)) → U11_GAA(X1, X2, X3, X4, hidden_flattenC_in_gaa(X2, X3, X4))
HIDDEN_FLATTENC_IN_GAA(.(X1, X2), X3, .(X1, X4)) → HIDDEN_FLATTENC_IN_GAA(X2, X3, X4)
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_in_gaa(X3, X4, X9))
U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → U4_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_gaagga(.(X1, X2), X9, X5, X6, X7, X8))
U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → PB_IN_GAAGGA(.(X1, X2), X9, X5, X6, X7, X8)
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U5_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattenC_in_gaa(X2, X3, X4))
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → HIDDEN_FLATTENC_IN_GAA(X2, X3, X4)
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_in_gaa(X2, X3, X4))
U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → U7_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattenA_in_gaa(.(X5, X6), .(X1, X4), X7))
U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → HIDDEN_FLATTENA_IN_GAA(.(X5, X6), .(X1, X4), X7)

The TRS R consists of the following rules:

hidden_flattencC_in_gaa([], X1, X1) → hidden_flattencC_out_gaa([], X1, X1)
hidden_flattencC_in_gaa(.(.(X1, X2), X3), X4, X5) → U24_gaa(X1, X2, X3, X4, X5, hidden_flattencC_in_gaa(X3, X4, X6))
hidden_flattencC_in_gaa(.(X1, X2), X3, .(X1, X4)) → U26_gaa(X1, X2, X3, X4, hidden_flattencC_in_gaa(X2, X3, X4))
U26_gaa(X1, X2, X3, X4, hidden_flattencC_out_gaa(X2, X3, X4)) → hidden_flattencC_out_gaa(.(X1, X2), X3, .(X1, X4))
U24_gaa(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → U25_gaa(X1, X2, X3, X4, X5, hidden_flattencA_in_gaa(.(X1, X2), X6, X5))
hidden_flattencA_in_gaa([], X1, X1) → hidden_flattencA_out_gaa([], X1, X1)
hidden_flattencA_in_gaa(.(.(X1, X2), X3), X4, X5) → U16_gaa(X1, X2, X3, X4, X5, qcB_in_gaagga(X3, X4, X6, X1, X2, X5))
qcB_in_gaagga([], X1, X1, X2, X3, X4) → U19_gaagga(X1, X2, X3, X4, hidden_flattencA_in_gaa(.(X2, X3), X1, X4))
hidden_flattencA_in_gaa(.(X1, []), X2, .(X1, X2)) → hidden_flattencA_out_gaa(.(X1, []), X2, .(X1, X2))
hidden_flattencA_in_gaa(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → U17_gaa(X1, X2, X3, X4, X5, X6, qcB_in_gaagga(X4, X5, X7, X2, X3, X6))
qcB_in_gaagga(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U20_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_in_gaa(X3, X4, X9))
U20_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → U21_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, qcB_in_gaagga(.(X1, X2), X9, X5, X6, X7, X8))
qcB_in_gaagga(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U22_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_in_gaa(X2, X3, X4))
U22_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → U23_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencA_in_gaa(.(X5, X6), .(X1, X4), X7))
hidden_flattencA_in_gaa(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → U18_gaa(X1, X2, X3, X4, X5, hidden_flattencA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, hidden_flattencA_out_gaa(X3, X4, X5)) → hidden_flattencA_out_gaa(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5)))
U23_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencA_out_gaa(.(X5, X6), .(X1, X4), X7)) → qcB_out_gaagga(.(X1, X2), X3, .(X1, X4), X5, X6, X7)
U21_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, qcB_out_gaagga(.(X1, X2), X9, X5, X6, X7, X8)) → qcB_out_gaagga(.(.(X1, X2), X3), X4, X5, X6, X7, X8)
U17_gaa(X1, X2, X3, X4, X5, X6, qcB_out_gaagga(X4, X5, X7, X2, X3, X6)) → hidden_flattencA_out_gaa(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6))
U19_gaagga(X1, X2, X3, X4, hidden_flattencA_out_gaa(.(X2, X3), X1, X4)) → qcB_out_gaagga([], X1, X1, X2, X3, X4)
U16_gaa(X1, X2, X3, X4, X5, qcB_out_gaagga(X3, X4, X6, X1, X2, X5)) → hidden_flattencA_out_gaa(.(.(X1, X2), X3), X4, X5)
U25_gaa(X1, X2, X3, X4, X5, hidden_flattencA_out_gaa(.(X1, X2), X6, X5)) → hidden_flattencC_out_gaa(.(.(X1, X2), X3), X4, X5)

The argument filtering Pi contains the following mapping:
hidden_flattenA_in_gaa(x1, x2, x3)  =  hidden_flattenA_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
pB_in_gaagga(x1, x2, x3, x4, x5, x6)  =  pB_in_gaagga(x1, x4, x5)
[]  =  []
hidden_flattenC_in_gaa(x1, x2, x3)  =  hidden_flattenC_in_gaa(x1)
hidden_flattencC_in_gaa(x1, x2, x3)  =  hidden_flattencC_in_gaa(x1)
hidden_flattencC_out_gaa(x1, x2, x3)  =  hidden_flattencC_out_gaa(x1)
U24_gaa(x1, x2, x3, x4, x5, x6)  =  U24_gaa(x1, x2, x3, x6)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
U25_gaa(x1, x2, x3, x4, x5, x6)  =  U25_gaa(x1, x2, x3, x6)
hidden_flattencA_in_gaa(x1, x2, x3)  =  hidden_flattencA_in_gaa(x1)
hidden_flattencA_out_gaa(x1, x2, x3)  =  hidden_flattencA_out_gaa(x1)
U16_gaa(x1, x2, x3, x4, x5, x6)  =  U16_gaa(x1, x2, x3, x6)
qcB_in_gaagga(x1, x2, x3, x4, x5, x6)  =  qcB_in_gaagga(x1, x4, x5)
U19_gaagga(x1, x2, x3, x4, x5)  =  U19_gaagga(x2, x3, x5)
U17_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U17_gaa(x1, x2, x3, x4, x7)
U20_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_gaagga(x1, x2, x3, x6, x7, x9)
U21_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U21_gaagga(x1, x2, x3, x6, x7, x9)
U22_gaagga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U22_gaagga(x1, x2, x5, x6, x8)
U23_gaagga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_gaagga(x1, x2, x5, x6, x8)
U18_gaa(x1, x2, x3, x4, x5, x6)  =  U18_gaa(x1, x2, x3, x6)
qcB_out_gaagga(x1, x2, x3, x4, x5, x6)  =  qcB_out_gaagga(x1, x4, x5)
HIDDEN_FLATTENA_IN_GAA(x1, x2, x3)  =  HIDDEN_FLATTENA_IN_GAA(x1)
U12_GAA(x1, x2, x3, x4, x5, x6)  =  U12_GAA(x1, x2, x3, x6)
PB_IN_GAAGGA(x1, x2, x3, x4, x5, x6)  =  PB_IN_GAAGGA(x1, x4, x5)
U1_GAAGGA(x1, x2, x3, x4, x5)  =  U1_GAAGGA(x2, x3, x5)
U13_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GAA(x1, x2, x3, x4, x7)
U2_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_GAAGGA(x1, x2, x3, x6, x7, x9)
HIDDEN_FLATTENC_IN_GAA(x1, x2, x3)  =  HIDDEN_FLATTENC_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5, x6)  =  U8_GAA(x1, x2, x3, x6)
U9_GAA(x1, x2, x3, x4, x5, x6)  =  U9_GAA(x1, x2, x3, x6)
U10_GAA(x1, x2, x3, x4, x5, x6)  =  U10_GAA(x1, x2, x3, x6)
U14_GAA(x1, x2, x3, x4, x5, x6)  =  U14_GAA(x1, x2, x3, x6)
U11_GAA(x1, x2, x3, x4, x5)  =  U11_GAA(x1, x2, x5)
U3_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_GAAGGA(x1, x2, x3, x6, x7, x9)
U4_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U4_GAAGGA(x1, x2, x3, x6, x7, x9)
U5_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U5_GAAGGA(x1, x2, x5, x6, x8)
U6_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U6_GAAGGA(x1, x2, x5, x6, x8)
U7_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U7_GAAGGA(x1, x2, x5, x6, x8)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3), X4, X5) → U12_GAA(X1, X2, X3, X4, X5, pB_in_gaagga(X3, X4, X6, X1, X2, X5))
HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3), X4, X5) → PB_IN_GAAGGA(X3, X4, X6, X1, X2, X5)
PB_IN_GAAGGA([], X1, X1, X2, X3, X4) → U1_GAAGGA(X1, X2, X3, X4, hidden_flattenA_in_gaa(.(X2, X3), X1, X4))
PB_IN_GAAGGA([], X1, X1, X2, X3, X4) → HIDDEN_FLATTENA_IN_GAA(.(X2, X3), X1, X4)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → U13_GAA(X1, X2, X3, X4, X5, X6, pB_in_gaagga(X4, X5, X7, X2, X3, X6))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → PB_IN_GAAGGA(X4, X5, X7, X2, X3, X6)
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U2_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattenC_in_gaa(X3, X4, X9))
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → HIDDEN_FLATTENC_IN_GAA(X3, X4, X9)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → U8_GAA(X1, X2, X3, X4, X5, hidden_flattenC_in_gaa(X3, X4, X6))
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → HIDDEN_FLATTENC_IN_GAA(X3, X4, X6)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_in_gaa(X3, X4, X6))
U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → U10_GAA(X1, X2, X3, X4, X5, hidden_flattenA_in_gaa(.(X1, X2), X6, X5))
U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → HIDDEN_FLATTENA_IN_GAA(.(X1, X2), X6, X5)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → U14_GAA(X1, X2, X3, X4, X5, hidden_flattenA_in_gaa(X3, X4, X5))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → HIDDEN_FLATTENA_IN_GAA(X3, X4, X5)
HIDDEN_FLATTENC_IN_GAA(.(X1, X2), X3, .(X1, X4)) → U11_GAA(X1, X2, X3, X4, hidden_flattenC_in_gaa(X2, X3, X4))
HIDDEN_FLATTENC_IN_GAA(.(X1, X2), X3, .(X1, X4)) → HIDDEN_FLATTENC_IN_GAA(X2, X3, X4)
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_in_gaa(X3, X4, X9))
U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → U4_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_gaagga(.(X1, X2), X9, X5, X6, X7, X8))
U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → PB_IN_GAAGGA(.(X1, X2), X9, X5, X6, X7, X8)
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U5_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattenC_in_gaa(X2, X3, X4))
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → HIDDEN_FLATTENC_IN_GAA(X2, X3, X4)
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_in_gaa(X2, X3, X4))
U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → U7_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattenA_in_gaa(.(X5, X6), .(X1, X4), X7))
U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → HIDDEN_FLATTENA_IN_GAA(.(X5, X6), .(X1, X4), X7)

The TRS R consists of the following rules:

hidden_flattencC_in_gaa([], X1, X1) → hidden_flattencC_out_gaa([], X1, X1)
hidden_flattencC_in_gaa(.(.(X1, X2), X3), X4, X5) → U24_gaa(X1, X2, X3, X4, X5, hidden_flattencC_in_gaa(X3, X4, X6))
hidden_flattencC_in_gaa(.(X1, X2), X3, .(X1, X4)) → U26_gaa(X1, X2, X3, X4, hidden_flattencC_in_gaa(X2, X3, X4))
U26_gaa(X1, X2, X3, X4, hidden_flattencC_out_gaa(X2, X3, X4)) → hidden_flattencC_out_gaa(.(X1, X2), X3, .(X1, X4))
U24_gaa(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → U25_gaa(X1, X2, X3, X4, X5, hidden_flattencA_in_gaa(.(X1, X2), X6, X5))
hidden_flattencA_in_gaa([], X1, X1) → hidden_flattencA_out_gaa([], X1, X1)
hidden_flattencA_in_gaa(.(.(X1, X2), X3), X4, X5) → U16_gaa(X1, X2, X3, X4, X5, qcB_in_gaagga(X3, X4, X6, X1, X2, X5))
qcB_in_gaagga([], X1, X1, X2, X3, X4) → U19_gaagga(X1, X2, X3, X4, hidden_flattencA_in_gaa(.(X2, X3), X1, X4))
hidden_flattencA_in_gaa(.(X1, []), X2, .(X1, X2)) → hidden_flattencA_out_gaa(.(X1, []), X2, .(X1, X2))
hidden_flattencA_in_gaa(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → U17_gaa(X1, X2, X3, X4, X5, X6, qcB_in_gaagga(X4, X5, X7, X2, X3, X6))
qcB_in_gaagga(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U20_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_in_gaa(X3, X4, X9))
U20_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → U21_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, qcB_in_gaagga(.(X1, X2), X9, X5, X6, X7, X8))
qcB_in_gaagga(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U22_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_in_gaa(X2, X3, X4))
U22_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → U23_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencA_in_gaa(.(X5, X6), .(X1, X4), X7))
hidden_flattencA_in_gaa(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → U18_gaa(X1, X2, X3, X4, X5, hidden_flattencA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, hidden_flattencA_out_gaa(X3, X4, X5)) → hidden_flattencA_out_gaa(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5)))
U23_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencA_out_gaa(.(X5, X6), .(X1, X4), X7)) → qcB_out_gaagga(.(X1, X2), X3, .(X1, X4), X5, X6, X7)
U21_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, qcB_out_gaagga(.(X1, X2), X9, X5, X6, X7, X8)) → qcB_out_gaagga(.(.(X1, X2), X3), X4, X5, X6, X7, X8)
U17_gaa(X1, X2, X3, X4, X5, X6, qcB_out_gaagga(X4, X5, X7, X2, X3, X6)) → hidden_flattencA_out_gaa(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6))
U19_gaagga(X1, X2, X3, X4, hidden_flattencA_out_gaa(.(X2, X3), X1, X4)) → qcB_out_gaagga([], X1, X1, X2, X3, X4)
U16_gaa(X1, X2, X3, X4, X5, qcB_out_gaagga(X3, X4, X6, X1, X2, X5)) → hidden_flattencA_out_gaa(.(.(X1, X2), X3), X4, X5)
U25_gaa(X1, X2, X3, X4, X5, hidden_flattencA_out_gaa(.(X1, X2), X6, X5)) → hidden_flattencC_out_gaa(.(.(X1, X2), X3), X4, X5)

The argument filtering Pi contains the following mapping:
hidden_flattenA_in_gaa(x1, x2, x3)  =  hidden_flattenA_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
pB_in_gaagga(x1, x2, x3, x4, x5, x6)  =  pB_in_gaagga(x1, x4, x5)
[]  =  []
hidden_flattenC_in_gaa(x1, x2, x3)  =  hidden_flattenC_in_gaa(x1)
hidden_flattencC_in_gaa(x1, x2, x3)  =  hidden_flattencC_in_gaa(x1)
hidden_flattencC_out_gaa(x1, x2, x3)  =  hidden_flattencC_out_gaa(x1)
U24_gaa(x1, x2, x3, x4, x5, x6)  =  U24_gaa(x1, x2, x3, x6)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
U25_gaa(x1, x2, x3, x4, x5, x6)  =  U25_gaa(x1, x2, x3, x6)
hidden_flattencA_in_gaa(x1, x2, x3)  =  hidden_flattencA_in_gaa(x1)
hidden_flattencA_out_gaa(x1, x2, x3)  =  hidden_flattencA_out_gaa(x1)
U16_gaa(x1, x2, x3, x4, x5, x6)  =  U16_gaa(x1, x2, x3, x6)
qcB_in_gaagga(x1, x2, x3, x4, x5, x6)  =  qcB_in_gaagga(x1, x4, x5)
U19_gaagga(x1, x2, x3, x4, x5)  =  U19_gaagga(x2, x3, x5)
U17_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U17_gaa(x1, x2, x3, x4, x7)
U20_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_gaagga(x1, x2, x3, x6, x7, x9)
U21_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U21_gaagga(x1, x2, x3, x6, x7, x9)
U22_gaagga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U22_gaagga(x1, x2, x5, x6, x8)
U23_gaagga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_gaagga(x1, x2, x5, x6, x8)
U18_gaa(x1, x2, x3, x4, x5, x6)  =  U18_gaa(x1, x2, x3, x6)
qcB_out_gaagga(x1, x2, x3, x4, x5, x6)  =  qcB_out_gaagga(x1, x4, x5)
HIDDEN_FLATTENA_IN_GAA(x1, x2, x3)  =  HIDDEN_FLATTENA_IN_GAA(x1)
U12_GAA(x1, x2, x3, x4, x5, x6)  =  U12_GAA(x1, x2, x3, x6)
PB_IN_GAAGGA(x1, x2, x3, x4, x5, x6)  =  PB_IN_GAAGGA(x1, x4, x5)
U1_GAAGGA(x1, x2, x3, x4, x5)  =  U1_GAAGGA(x2, x3, x5)
U13_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GAA(x1, x2, x3, x4, x7)
U2_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_GAAGGA(x1, x2, x3, x6, x7, x9)
HIDDEN_FLATTENC_IN_GAA(x1, x2, x3)  =  HIDDEN_FLATTENC_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5, x6)  =  U8_GAA(x1, x2, x3, x6)
U9_GAA(x1, x2, x3, x4, x5, x6)  =  U9_GAA(x1, x2, x3, x6)
U10_GAA(x1, x2, x3, x4, x5, x6)  =  U10_GAA(x1, x2, x3, x6)
U14_GAA(x1, x2, x3, x4, x5, x6)  =  U14_GAA(x1, x2, x3, x6)
U11_GAA(x1, x2, x3, x4, x5)  =  U11_GAA(x1, x2, x5)
U3_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_GAAGGA(x1, x2, x3, x6, x7, x9)
U4_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U4_GAAGGA(x1, x2, x3, x6, x7, x9)
U5_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U5_GAAGGA(x1, x2, x5, x6, x8)
U6_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U6_GAAGGA(x1, x2, x5, x6, x8)
U7_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U7_GAAGGA(x1, x2, x5, x6, x8)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 11 less nodes.

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3), X4, X5) → PB_IN_GAAGGA(X3, X4, X6, X1, X2, X5)
PB_IN_GAAGGA([], X1, X1, X2, X3, X4) → HIDDEN_FLATTENA_IN_GAA(.(X2, X3), X1, X4)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → PB_IN_GAAGGA(X4, X5, X7, X2, X3, X6)
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → HIDDEN_FLATTENC_IN_GAA(X3, X4, X9)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → HIDDEN_FLATTENC_IN_GAA(X3, X4, X6)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3), X4, X5) → U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_in_gaa(X3, X4, X6))
U9_GAA(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → HIDDEN_FLATTENA_IN_GAA(.(X1, X2), X6, X5)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → HIDDEN_FLATTENA_IN_GAA(X3, X4, X5)
HIDDEN_FLATTENC_IN_GAA(.(X1, X2), X3, .(X1, X4)) → HIDDEN_FLATTENC_IN_GAA(X2, X3, X4)
PB_IN_GAAGGA(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_in_gaa(X3, X4, X9))
U3_GAAGGA(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → PB_IN_GAAGGA(.(X1, X2), X9, X5, X6, X7, X8)
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → HIDDEN_FLATTENC_IN_GAA(X2, X3, X4)
PB_IN_GAAGGA(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_in_gaa(X2, X3, X4))
U6_GAAGGA(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → HIDDEN_FLATTENA_IN_GAA(.(X5, X6), .(X1, X4), X7)

The TRS R consists of the following rules:

hidden_flattencC_in_gaa([], X1, X1) → hidden_flattencC_out_gaa([], X1, X1)
hidden_flattencC_in_gaa(.(.(X1, X2), X3), X4, X5) → U24_gaa(X1, X2, X3, X4, X5, hidden_flattencC_in_gaa(X3, X4, X6))
hidden_flattencC_in_gaa(.(X1, X2), X3, .(X1, X4)) → U26_gaa(X1, X2, X3, X4, hidden_flattencC_in_gaa(X2, X3, X4))
U26_gaa(X1, X2, X3, X4, hidden_flattencC_out_gaa(X2, X3, X4)) → hidden_flattencC_out_gaa(.(X1, X2), X3, .(X1, X4))
U24_gaa(X1, X2, X3, X4, X5, hidden_flattencC_out_gaa(X3, X4, X6)) → U25_gaa(X1, X2, X3, X4, X5, hidden_flattencA_in_gaa(.(X1, X2), X6, X5))
hidden_flattencA_in_gaa([], X1, X1) → hidden_flattencA_out_gaa([], X1, X1)
hidden_flattencA_in_gaa(.(.(X1, X2), X3), X4, X5) → U16_gaa(X1, X2, X3, X4, X5, qcB_in_gaagga(X3, X4, X6, X1, X2, X5))
qcB_in_gaagga([], X1, X1, X2, X3, X4) → U19_gaagga(X1, X2, X3, X4, hidden_flattencA_in_gaa(.(X2, X3), X1, X4))
hidden_flattencA_in_gaa(.(X1, []), X2, .(X1, X2)) → hidden_flattencA_out_gaa(.(X1, []), X2, .(X1, X2))
hidden_flattencA_in_gaa(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6)) → U17_gaa(X1, X2, X3, X4, X5, X6, qcB_in_gaagga(X4, X5, X7, X2, X3, X6))
qcB_in_gaagga(.(.(X1, X2), X3), X4, X5, X6, X7, X8) → U20_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_in_gaa(X3, X4, X9))
U20_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, hidden_flattencC_out_gaa(X3, X4, X9)) → U21_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, qcB_in_gaagga(.(X1, X2), X9, X5, X6, X7, X8))
qcB_in_gaagga(.(X1, X2), X3, .(X1, X4), X5, X6, X7) → U22_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_in_gaa(X2, X3, X4))
U22_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencC_out_gaa(X2, X3, X4)) → U23_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencA_in_gaa(.(X5, X6), .(X1, X4), X7))
hidden_flattencA_in_gaa(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5))) → U18_gaa(X1, X2, X3, X4, X5, hidden_flattencA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, hidden_flattencA_out_gaa(X3, X4, X5)) → hidden_flattencA_out_gaa(.(X1, .(X2, X3)), X4, .(X1, .(X2, X5)))
U23_gaagga(X1, X2, X3, X4, X5, X6, X7, hidden_flattencA_out_gaa(.(X5, X6), .(X1, X4), X7)) → qcB_out_gaagga(.(X1, X2), X3, .(X1, X4), X5, X6, X7)
U21_gaagga(X1, X2, X3, X4, X5, X6, X7, X8, qcB_out_gaagga(.(X1, X2), X9, X5, X6, X7, X8)) → qcB_out_gaagga(.(.(X1, X2), X3), X4, X5, X6, X7, X8)
U17_gaa(X1, X2, X3, X4, X5, X6, qcB_out_gaagga(X4, X5, X7, X2, X3, X6)) → hidden_flattencA_out_gaa(.(X1, .(.(X2, X3), X4)), X5, .(X1, X6))
U19_gaagga(X1, X2, X3, X4, hidden_flattencA_out_gaa(.(X2, X3), X1, X4)) → qcB_out_gaagga([], X1, X1, X2, X3, X4)
U16_gaa(X1, X2, X3, X4, X5, qcB_out_gaagga(X3, X4, X6, X1, X2, X5)) → hidden_flattencA_out_gaa(.(.(X1, X2), X3), X4, X5)
U25_gaa(X1, X2, X3, X4, X5, hidden_flattencA_out_gaa(.(X1, X2), X6, X5)) → hidden_flattencC_out_gaa(.(.(X1, X2), X3), X4, X5)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
hidden_flattencC_in_gaa(x1, x2, x3)  =  hidden_flattencC_in_gaa(x1)
hidden_flattencC_out_gaa(x1, x2, x3)  =  hidden_flattencC_out_gaa(x1)
U24_gaa(x1, x2, x3, x4, x5, x6)  =  U24_gaa(x1, x2, x3, x6)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
U25_gaa(x1, x2, x3, x4, x5, x6)  =  U25_gaa(x1, x2, x3, x6)
hidden_flattencA_in_gaa(x1, x2, x3)  =  hidden_flattencA_in_gaa(x1)
hidden_flattencA_out_gaa(x1, x2, x3)  =  hidden_flattencA_out_gaa(x1)
U16_gaa(x1, x2, x3, x4, x5, x6)  =  U16_gaa(x1, x2, x3, x6)
qcB_in_gaagga(x1, x2, x3, x4, x5, x6)  =  qcB_in_gaagga(x1, x4, x5)
U19_gaagga(x1, x2, x3, x4, x5)  =  U19_gaagga(x2, x3, x5)
U17_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U17_gaa(x1, x2, x3, x4, x7)
U20_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_gaagga(x1, x2, x3, x6, x7, x9)
U21_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U21_gaagga(x1, x2, x3, x6, x7, x9)
U22_gaagga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U22_gaagga(x1, x2, x5, x6, x8)
U23_gaagga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_gaagga(x1, x2, x5, x6, x8)
U18_gaa(x1, x2, x3, x4, x5, x6)  =  U18_gaa(x1, x2, x3, x6)
qcB_out_gaagga(x1, x2, x3, x4, x5, x6)  =  qcB_out_gaagga(x1, x4, x5)
HIDDEN_FLATTENA_IN_GAA(x1, x2, x3)  =  HIDDEN_FLATTENA_IN_GAA(x1)
PB_IN_GAAGGA(x1, x2, x3, x4, x5, x6)  =  PB_IN_GAAGGA(x1, x4, x5)
HIDDEN_FLATTENC_IN_GAA(x1, x2, x3)  =  HIDDEN_FLATTENC_IN_GAA(x1)
U9_GAA(x1, x2, x3, x4, x5, x6)  =  U9_GAA(x1, x2, x3, x6)
U3_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_GAAGGA(x1, x2, x3, x6, x7, x9)
U6_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U6_GAAGGA(x1, x2, x5, x6, x8)

We have to consider all (P,R,Pi)-chains

(7) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3)) → PB_IN_GAAGGA(X3, X1, X2)
PB_IN_GAAGGA([], X2, X3) → HIDDEN_FLATTENA_IN_GAA(.(X2, X3))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4))) → PB_IN_GAAGGA(X4, X2, X3)
PB_IN_GAAGGA(.(.(X1, X2), X3), X6, X7) → HIDDEN_FLATTENC_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3)) → HIDDEN_FLATTENC_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3)) → U9_GAA(X1, X2, X3, hidden_flattencC_in_gaa(X3))
U9_GAA(X1, X2, X3, hidden_flattencC_out_gaa(X3)) → HIDDEN_FLATTENA_IN_GAA(.(X1, X2))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3))) → HIDDEN_FLATTENA_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(X1, X2)) → HIDDEN_FLATTENC_IN_GAA(X2)
PB_IN_GAAGGA(.(.(X1, X2), X3), X6, X7) → U3_GAAGGA(X1, X2, X3, X6, X7, hidden_flattencC_in_gaa(X3))
U3_GAAGGA(X1, X2, X3, X6, X7, hidden_flattencC_out_gaa(X3)) → PB_IN_GAAGGA(.(X1, X2), X6, X7)
PB_IN_GAAGGA(.(X1, X2), X5, X6) → HIDDEN_FLATTENC_IN_GAA(X2)
PB_IN_GAAGGA(.(X1, X2), X5, X6) → U6_GAAGGA(X1, X2, X5, X6, hidden_flattencC_in_gaa(X2))
U6_GAAGGA(X1, X2, X5, X6, hidden_flattencC_out_gaa(X2)) → HIDDEN_FLATTENA_IN_GAA(.(X5, X6))

The TRS R consists of the following rules:

hidden_flattencC_in_gaa([]) → hidden_flattencC_out_gaa([])
hidden_flattencC_in_gaa(.(.(X1, X2), X3)) → U24_gaa(X1, X2, X3, hidden_flattencC_in_gaa(X3))
hidden_flattencC_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, hidden_flattencC_in_gaa(X2))
U26_gaa(X1, X2, hidden_flattencC_out_gaa(X2)) → hidden_flattencC_out_gaa(.(X1, X2))
U24_gaa(X1, X2, X3, hidden_flattencC_out_gaa(X3)) → U25_gaa(X1, X2, X3, hidden_flattencA_in_gaa(.(X1, X2)))
hidden_flattencA_in_gaa([]) → hidden_flattencA_out_gaa([])
hidden_flattencA_in_gaa(.(.(X1, X2), X3)) → U16_gaa(X1, X2, X3, qcB_in_gaagga(X3, X1, X2))
qcB_in_gaagga([], X2, X3) → U19_gaagga(X2, X3, hidden_flattencA_in_gaa(.(X2, X3)))
hidden_flattencA_in_gaa(.(X1, [])) → hidden_flattencA_out_gaa(.(X1, []))
hidden_flattencA_in_gaa(.(X1, .(.(X2, X3), X4))) → U17_gaa(X1, X2, X3, X4, qcB_in_gaagga(X4, X2, X3))
qcB_in_gaagga(.(.(X1, X2), X3), X6, X7) → U20_gaagga(X1, X2, X3, X6, X7, hidden_flattencC_in_gaa(X3))
U20_gaagga(X1, X2, X3, X6, X7, hidden_flattencC_out_gaa(X3)) → U21_gaagga(X1, X2, X3, X6, X7, qcB_in_gaagga(.(X1, X2), X6, X7))
qcB_in_gaagga(.(X1, X2), X5, X6) → U22_gaagga(X1, X2, X5, X6, hidden_flattencC_in_gaa(X2))
U22_gaagga(X1, X2, X5, X6, hidden_flattencC_out_gaa(X2)) → U23_gaagga(X1, X2, X5, X6, hidden_flattencA_in_gaa(.(X5, X6)))
hidden_flattencA_in_gaa(.(X1, .(X2, X3))) → U18_gaa(X1, X2, X3, hidden_flattencA_in_gaa(X3))
U18_gaa(X1, X2, X3, hidden_flattencA_out_gaa(X3)) → hidden_flattencA_out_gaa(.(X1, .(X2, X3)))
U23_gaagga(X1, X2, X5, X6, hidden_flattencA_out_gaa(.(X5, X6))) → qcB_out_gaagga(.(X1, X2), X5, X6)
U21_gaagga(X1, X2, X3, X6, X7, qcB_out_gaagga(.(X1, X2), X6, X7)) → qcB_out_gaagga(.(.(X1, X2), X3), X6, X7)
U17_gaa(X1, X2, X3, X4, qcB_out_gaagga(X4, X2, X3)) → hidden_flattencA_out_gaa(.(X1, .(.(X2, X3), X4)))
U19_gaagga(X2, X3, hidden_flattencA_out_gaa(.(X2, X3))) → qcB_out_gaagga([], X2, X3)
U16_gaa(X1, X2, X3, qcB_out_gaagga(X3, X1, X2)) → hidden_flattencA_out_gaa(.(.(X1, X2), X3))
U25_gaa(X1, X2, X3, hidden_flattencA_out_gaa(.(X1, X2))) → hidden_flattencC_out_gaa(.(.(X1, X2), X3))

The set Q consists of the following terms:

hidden_flattencC_in_gaa(x0)
U26_gaa(x0, x1, x2)
U24_gaa(x0, x1, x2, x3)
hidden_flattencA_in_gaa(x0)
qcB_in_gaagga(x0, x1, x2)
U20_gaagga(x0, x1, x2, x3, x4, x5)
U22_gaagga(x0, x1, x2, x3, x4)
U18_gaa(x0, x1, x2, x3)
U23_gaagga(x0, x1, x2, x3, x4)
U21_gaagga(x0, x1, x2, x3, x4, x5)
U17_gaa(x0, x1, x2, x3, x4)
U19_gaagga(x0, x1, x2)
U16_gaa(x0, x1, x2, x3)
U25_gaa(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PB_IN_GAAGGA([], X2, X3) → HIDDEN_FLATTENA_IN_GAA(.(X2, X3))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1 + x2   
POL(HIDDEN_FLATTENA_IN_GAA(x1)) = x1   
POL(HIDDEN_FLATTENC_IN_GAA(x1)) = x1   
POL(PB_IN_GAAGGA(x1, x2, x3)) = x1 + x2 + x3   
POL(U16_gaa(x1, x2, x3, x4)) = 0   
POL(U17_gaa(x1, x2, x3, x4, x5)) = 0   
POL(U18_gaa(x1, x2, x3, x4)) = 0   
POL(U19_gaagga(x1, x2, x3)) = 0   
POL(U20_gaagga(x1, x2, x3, x4, x5, x6)) = 0   
POL(U21_gaagga(x1, x2, x3, x4, x5, x6)) = 0   
POL(U22_gaagga(x1, x2, x3, x4, x5)) = 0   
POL(U23_gaagga(x1, x2, x3, x4, x5)) = 0   
POL(U24_gaa(x1, x2, x3, x4)) = 0   
POL(U25_gaa(x1, x2, x3, x4)) = 0   
POL(U26_gaa(x1, x2, x3)) = 0   
POL(U3_GAAGGA(x1, x2, x3, x4, x5, x6)) = x1 + x2 + x4 + x5   
POL(U6_GAAGGA(x1, x2, x3, x4, x5)) = x3 + x4   
POL(U9_GAA(x1, x2, x3, x4)) = x1 + x2 + x3   
POL([]) = 1   
POL(hidden_flattencA_in_gaa(x1)) = 1 + x1   
POL(hidden_flattencA_out_gaa(x1)) = x1   
POL(hidden_flattencC_in_gaa(x1)) = 0   
POL(hidden_flattencC_out_gaa(x1)) = 0   
POL(qcB_in_gaagga(x1, x2, x3)) = 0   
POL(qcB_out_gaagga(x1, x2, x3)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3)) → PB_IN_GAAGGA(X3, X1, X2)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4))) → PB_IN_GAAGGA(X4, X2, X3)
PB_IN_GAAGGA(.(.(X1, X2), X3), X6, X7) → HIDDEN_FLATTENC_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3)) → HIDDEN_FLATTENC_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3)) → U9_GAA(X1, X2, X3, hidden_flattencC_in_gaa(X3))
U9_GAA(X1, X2, X3, hidden_flattencC_out_gaa(X3)) → HIDDEN_FLATTENA_IN_GAA(.(X1, X2))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3))) → HIDDEN_FLATTENA_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(X1, X2)) → HIDDEN_FLATTENC_IN_GAA(X2)
PB_IN_GAAGGA(.(.(X1, X2), X3), X6, X7) → U3_GAAGGA(X1, X2, X3, X6, X7, hidden_flattencC_in_gaa(X3))
U3_GAAGGA(X1, X2, X3, X6, X7, hidden_flattencC_out_gaa(X3)) → PB_IN_GAAGGA(.(X1, X2), X6, X7)
PB_IN_GAAGGA(.(X1, X2), X5, X6) → HIDDEN_FLATTENC_IN_GAA(X2)
PB_IN_GAAGGA(.(X1, X2), X5, X6) → U6_GAAGGA(X1, X2, X5, X6, hidden_flattencC_in_gaa(X2))
U6_GAAGGA(X1, X2, X5, X6, hidden_flattencC_out_gaa(X2)) → HIDDEN_FLATTENA_IN_GAA(.(X5, X6))

The TRS R consists of the following rules:

hidden_flattencC_in_gaa([]) → hidden_flattencC_out_gaa([])
hidden_flattencC_in_gaa(.(.(X1, X2), X3)) → U24_gaa(X1, X2, X3, hidden_flattencC_in_gaa(X3))
hidden_flattencC_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, hidden_flattencC_in_gaa(X2))
U26_gaa(X1, X2, hidden_flattencC_out_gaa(X2)) → hidden_flattencC_out_gaa(.(X1, X2))
U24_gaa(X1, X2, X3, hidden_flattencC_out_gaa(X3)) → U25_gaa(X1, X2, X3, hidden_flattencA_in_gaa(.(X1, X2)))
hidden_flattencA_in_gaa([]) → hidden_flattencA_out_gaa([])
hidden_flattencA_in_gaa(.(.(X1, X2), X3)) → U16_gaa(X1, X2, X3, qcB_in_gaagga(X3, X1, X2))
qcB_in_gaagga([], X2, X3) → U19_gaagga(X2, X3, hidden_flattencA_in_gaa(.(X2, X3)))
hidden_flattencA_in_gaa(.(X1, [])) → hidden_flattencA_out_gaa(.(X1, []))
hidden_flattencA_in_gaa(.(X1, .(.(X2, X3), X4))) → U17_gaa(X1, X2, X3, X4, qcB_in_gaagga(X4, X2, X3))
qcB_in_gaagga(.(.(X1, X2), X3), X6, X7) → U20_gaagga(X1, X2, X3, X6, X7, hidden_flattencC_in_gaa(X3))
U20_gaagga(X1, X2, X3, X6, X7, hidden_flattencC_out_gaa(X3)) → U21_gaagga(X1, X2, X3, X6, X7, qcB_in_gaagga(.(X1, X2), X6, X7))
qcB_in_gaagga(.(X1, X2), X5, X6) → U22_gaagga(X1, X2, X5, X6, hidden_flattencC_in_gaa(X2))
U22_gaagga(X1, X2, X5, X6, hidden_flattencC_out_gaa(X2)) → U23_gaagga(X1, X2, X5, X6, hidden_flattencA_in_gaa(.(X5, X6)))
hidden_flattencA_in_gaa(.(X1, .(X2, X3))) → U18_gaa(X1, X2, X3, hidden_flattencA_in_gaa(X3))
U18_gaa(X1, X2, X3, hidden_flattencA_out_gaa(X3)) → hidden_flattencA_out_gaa(.(X1, .(X2, X3)))
U23_gaagga(X1, X2, X5, X6, hidden_flattencA_out_gaa(.(X5, X6))) → qcB_out_gaagga(.(X1, X2), X5, X6)
U21_gaagga(X1, X2, X3, X6, X7, qcB_out_gaagga(.(X1, X2), X6, X7)) → qcB_out_gaagga(.(.(X1, X2), X3), X6, X7)
U17_gaa(X1, X2, X3, X4, qcB_out_gaagga(X4, X2, X3)) → hidden_flattencA_out_gaa(.(X1, .(.(X2, X3), X4)))
U19_gaagga(X2, X3, hidden_flattencA_out_gaa(.(X2, X3))) → qcB_out_gaagga([], X2, X3)
U16_gaa(X1, X2, X3, qcB_out_gaagga(X3, X1, X2)) → hidden_flattencA_out_gaa(.(.(X1, X2), X3))
U25_gaa(X1, X2, X3, hidden_flattencA_out_gaa(.(X1, X2))) → hidden_flattencC_out_gaa(.(.(X1, X2), X3))

The set Q consists of the following terms:

hidden_flattencC_in_gaa(x0)
U26_gaa(x0, x1, x2)
U24_gaa(x0, x1, x2, x3)
hidden_flattencA_in_gaa(x0)
qcB_in_gaagga(x0, x1, x2)
U20_gaagga(x0, x1, x2, x3, x4, x5)
U22_gaagga(x0, x1, x2, x3, x4)
U18_gaa(x0, x1, x2, x3)
U23_gaagga(x0, x1, x2, x3, x4)
U21_gaagga(x0, x1, x2, x3, x4, x5)
U17_gaa(x0, x1, x2, x3, x4)
U19_gaagga(x0, x1, x2)
U16_gaa(x0, x1, x2, x3)
U25_gaa(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


HIDDEN_FLATTENA_IN_GAA(.(.(X1, X2), X3)) → PB_IN_GAAGGA(X3, X1, X2)
HIDDEN_FLATTENA_IN_GAA(.(X1, .(.(X2, X3), X4))) → PB_IN_GAAGGA(X4, X2, X3)
PB_IN_GAAGGA(.(.(X1, X2), X3), X6, X7) → HIDDEN_FLATTENC_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3)) → HIDDEN_FLATTENC_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(.(X1, X2), X3)) → U9_GAA(X1, X2, X3, hidden_flattencC_in_gaa(X3))
HIDDEN_FLATTENA_IN_GAA(.(X1, .(X2, X3))) → HIDDEN_FLATTENA_IN_GAA(X3)
HIDDEN_FLATTENC_IN_GAA(.(X1, X2)) → HIDDEN_FLATTENC_IN_GAA(X2)
PB_IN_GAAGGA(.(.(X1, X2), X3), X6, X7) → U3_GAAGGA(X1, X2, X3, X6, X7, hidden_flattencC_in_gaa(X3))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x1 + x2   
POL(HIDDEN_FLATTENA_IN_GAA(x1)) = x1   
POL(HIDDEN_FLATTENC_IN_GAA(x1)) = 1 + x1   
POL(PB_IN_GAAGGA(x1, x2, x3)) = x1 + x2 + x3   
POL(U16_gaa(x1, x2, x3, x4)) = 0   
POL(U17_gaa(x1, x2, x3, x4, x5)) = 0   
POL(U18_gaa(x1, x2, x3, x4)) = 0   
POL(U19_gaagga(x1, x2, x3)) = 0   
POL(U20_gaagga(x1, x2, x3, x4, x5, x6)) = 0   
POL(U21_gaagga(x1, x2, x3, x4, x5, x6)) = 0   
POL(U22_gaagga(x1, x2, x3, x4, x5)) = 0   
POL(U23_gaagga(x1, x2, x3, x4, x5)) = 0   
POL(U24_gaa(x1, x2, x3, x4)) = 0   
POL(U25_gaa(x1, x2, x3, x4)) = 0   
POL(U26_gaa(x1, x2, x3)) = 0   
POL(U3_GAAGGA(x1, x2, x3, x4, x5, x6)) = 1 + x1 + x2 + x4 + x5   
POL(U6_GAAGGA(x1, x2, x3, x4, x5)) = 1 + x3 + x4   
POL(U9_GAA(x1, x2, x3, x4)) = 1 + x1 + x2   
POL([]) = 1   
POL(hidden_flattencA_in_gaa(x1)) = 1 + x1   
POL(hidden_flattencA_out_gaa(x1)) = x1   
POL(hidden_flattencC_in_gaa(x1)) = 0   
POL(hidden_flattencC_out_gaa(x1)) = 0   
POL(qcB_in_gaagga(x1, x2, x3)) = 0   
POL(qcB_out_gaagga(x1, x2, x3)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U9_GAA(X1, X2, X3, hidden_flattencC_out_gaa(X3)) → HIDDEN_FLATTENA_IN_GAA(.(X1, X2))
U3_GAAGGA(X1, X2, X3, X6, X7, hidden_flattencC_out_gaa(X3)) → PB_IN_GAAGGA(.(X1, X2), X6, X7)
PB_IN_GAAGGA(.(X1, X2), X5, X6) → HIDDEN_FLATTENC_IN_GAA(X2)
PB_IN_GAAGGA(.(X1, X2), X5, X6) → U6_GAAGGA(X1, X2, X5, X6, hidden_flattencC_in_gaa(X2))
U6_GAAGGA(X1, X2, X5, X6, hidden_flattencC_out_gaa(X2)) → HIDDEN_FLATTENA_IN_GAA(.(X5, X6))

The TRS R consists of the following rules:

hidden_flattencC_in_gaa([]) → hidden_flattencC_out_gaa([])
hidden_flattencC_in_gaa(.(.(X1, X2), X3)) → U24_gaa(X1, X2, X3, hidden_flattencC_in_gaa(X3))
hidden_flattencC_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, hidden_flattencC_in_gaa(X2))
U26_gaa(X1, X2, hidden_flattencC_out_gaa(X2)) → hidden_flattencC_out_gaa(.(X1, X2))
U24_gaa(X1, X2, X3, hidden_flattencC_out_gaa(X3)) → U25_gaa(X1, X2, X3, hidden_flattencA_in_gaa(.(X1, X2)))
hidden_flattencA_in_gaa([]) → hidden_flattencA_out_gaa([])
hidden_flattencA_in_gaa(.(.(X1, X2), X3)) → U16_gaa(X1, X2, X3, qcB_in_gaagga(X3, X1, X2))
qcB_in_gaagga([], X2, X3) → U19_gaagga(X2, X3, hidden_flattencA_in_gaa(.(X2, X3)))
hidden_flattencA_in_gaa(.(X1, [])) → hidden_flattencA_out_gaa(.(X1, []))
hidden_flattencA_in_gaa(.(X1, .(.(X2, X3), X4))) → U17_gaa(X1, X2, X3, X4, qcB_in_gaagga(X4, X2, X3))
qcB_in_gaagga(.(.(X1, X2), X3), X6, X7) → U20_gaagga(X1, X2, X3, X6, X7, hidden_flattencC_in_gaa(X3))
U20_gaagga(X1, X2, X3, X6, X7, hidden_flattencC_out_gaa(X3)) → U21_gaagga(X1, X2, X3, X6, X7, qcB_in_gaagga(.(X1, X2), X6, X7))
qcB_in_gaagga(.(X1, X2), X5, X6) → U22_gaagga(X1, X2, X5, X6, hidden_flattencC_in_gaa(X2))
U22_gaagga(X1, X2, X5, X6, hidden_flattencC_out_gaa(X2)) → U23_gaagga(X1, X2, X5, X6, hidden_flattencA_in_gaa(.(X5, X6)))
hidden_flattencA_in_gaa(.(X1, .(X2, X3))) → U18_gaa(X1, X2, X3, hidden_flattencA_in_gaa(X3))
U18_gaa(X1, X2, X3, hidden_flattencA_out_gaa(X3)) → hidden_flattencA_out_gaa(.(X1, .(X2, X3)))
U23_gaagga(X1, X2, X5, X6, hidden_flattencA_out_gaa(.(X5, X6))) → qcB_out_gaagga(.(X1, X2), X5, X6)
U21_gaagga(X1, X2, X3, X6, X7, qcB_out_gaagga(.(X1, X2), X6, X7)) → qcB_out_gaagga(.(.(X1, X2), X3), X6, X7)
U17_gaa(X1, X2, X3, X4, qcB_out_gaagga(X4, X2, X3)) → hidden_flattencA_out_gaa(.(X1, .(.(X2, X3), X4)))
U19_gaagga(X2, X3, hidden_flattencA_out_gaa(.(X2, X3))) → qcB_out_gaagga([], X2, X3)
U16_gaa(X1, X2, X3, qcB_out_gaagga(X3, X1, X2)) → hidden_flattencA_out_gaa(.(.(X1, X2), X3))
U25_gaa(X1, X2, X3, hidden_flattencA_out_gaa(.(X1, X2))) → hidden_flattencC_out_gaa(.(.(X1, X2), X3))

The set Q consists of the following terms:

hidden_flattencC_in_gaa(x0)
U26_gaa(x0, x1, x2)
U24_gaa(x0, x1, x2, x3)
hidden_flattencA_in_gaa(x0)
qcB_in_gaagga(x0, x1, x2)
U20_gaagga(x0, x1, x2, x3, x4, x5)
U22_gaagga(x0, x1, x2, x3, x4)
U18_gaa(x0, x1, x2, x3)
U23_gaagga(x0, x1, x2, x3, x4)
U21_gaagga(x0, x1, x2, x3, x4, x5)
U17_gaa(x0, x1, x2, x3, x4)
U19_gaagga(x0, x1, x2)
U16_gaa(x0, x1, x2, x3)
U25_gaa(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(13) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 5 less nodes.

(14) TRUE